Step of Proof: fseg_select 11,40

Inference at * 2 1 1 1 2 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
6. i : 
7. i < ||l1||
  l1[i] = nth_tl(||l2|| - ||l1||;l2)[i
latex

 by ((RWO "select_nth_tl" 0) 
CollapseTHEN (Auto')) 
latex


C1

C1:   l1[i] = l2[(i+(||l2|| - ||l1||))]
C.


Definitionsnth_tl(n;as), P  Q, P  Q, l[i], S  T, |g|, {i..j}, A, False, P  Q, n - m, i  j < k, P & Q, x:A  B(x), , #$n, t  T, a < b, , {x:AB(x)} , , x:AB(x), x:AB(x), A  B, type List, Type, s = t, ||as||, i  j 
Lemmasiff wf, rev implies wf, select nth tl, select wf, le wf

origin